T:Type, eq, r:(TT).
(a, b:T. ((eq(a,b)))  (a = b))
 Linorder(T;a,b.(r(a,b)))
 (x:T, L:(T List).
 sorted-by(x,y. (r(x,y));L)  no_repeats(T;L)  no_repeats(T;insert-by(eq;r;x;L))) 

latex

Definitions

type List, t  T, s = t, Type, x:AB(x), x:A. B(x), Linorder(T;x,y.R(x;y)), b, sorted-by(R;L), no_repeats(T;l), P  Q, f(a), , x.A(x), x,y. t(x;y), P  Q, , insert-by(eq;r;x;l), P & Q, x:A  B(x), P  Q, [car / cdr], S  T, |g|, A, #$n, {x:A| B(x)} , l[i], ||as||, [], , , A  B, {i..j}, a < b, (x  l), Void, False, ff, b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], p  q, p  q, p q, tt, Unit, left + right, if b then t else f fi , A List, xL. P(x), P  Q, <a, b>, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), case b of inl(x) => s(x) | inr(y) => t(y)

Lemmas

member-insert-by, false wf, cons member, sorted-by-cons, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, no repeats cons, insert-by wf, l member wf, length wf2, select wf, int seg wf, not wf, nat wf, bool wf, iff wf, linorder wf, no repeats wf, assert wf, sorted-by wf